Search for: All records

Quantum computing technology may soon deliver revolutionary improvements in algorithmic performance, but it is useful only if computed answers are correct. While hardware-level decoherence errors have garnered significant attention, a less recognized obstacle to correctness is that of human programming errors—“bugs.” Techniques familiar to most programmers from the classical domain for avoiding, discovering, and diagnosing bugs do not easily transfer, at scale, to the quantum domain because of its unique characteristics. To address this problem, we have been working to adapt formal methods to quantum programming. With such methods, a programmer writes a mathematical specification alongside the program and semiautomatically proves the program correct with respect to it. The proof’s validity is automatically confirmed—certified—by a “proof assistant.” Formal methods have successfully yielded high-assurance classical software artifacts, and the underlying technology has produced certified proofs of major mathematical theorems. As a demonstration of the feasibility of applying formal methods to quantum programming, we present a formally certified end-to-end implementation of Shor’s prime factorization algorithm, developed as part of a framework for applying the certified approach to general applications. By leveraging our framework, one can significantly reduce the effects of human errors and obtain a high-assurance implementation of large-scale quantum applications in a principled way. 

We formulate the first differentiable analog quantum computing framework with specific parameterization design at the analog signal (pulse) level to better exploit near-term quantum devices via variational methods. We further propose a scalable approach to estimate the gradients of quantum dynamics using a forward pass with Monte Carlo sampling, which leads to a quantum stochastic gradient descent algorithm for scalable gradient-based training in our framework. Applying our framework to quantum optimization and control, we observe a significant advantage of differentiable analog quantum computing against SOTAs based on parameterized digital quantum circuits by {\em orders of magnitude}. 

Abstract Ionospheric irregularities can adversely affect the performance of Global Navigation Satellite System (GNSS). However, this opens the possibility of using GNSS as an effective ionospheric remote sensing tool. Despite ionospheric monitoring has been undertaken for decades, these irregularities in multiple spatial and temporal scales are still not fully understood. This paper reviews Virginia Tech’s recent studies on multi-scale ionospheric irregularities using ground-based and space-based GNSS observations. First, the relevant background of ionospheric irregularities and their impact on GNSS signals is reviewed. Next, three topics of ground-based observations of ionospheric irregularities for which GNSS and other ground-based techniques are used simultaneously are reviewed. Both passive and active measurements in high-latitude regions are covered. Modelling and observations in mid-latitude regions are considered as well. Emphasis is placed on the increased capability of assessing the multi-scale nature of ionospheric irregularities using other traditional techniques (e.g., radar, magnetometer, high frequency receivers) as well as GNSS observations (e.g., Total-Electron-Content or TEC, scintillation). Besides ground-based observations, recent advances in GNSS space-based ionospheric measurements are briefly reviewed. Finally, a new space-based ionospheric observation technique using GNSS-based spacecraft formation flying and a differential TEC method is demonstrated using the newly developed Virginia Tech Formation Flying Testbed (VTFFTB). Based on multi-constellation multi-band GNSS, the VTFFTB has been developed into a hardware-in-the-loop simulation testbed with external high-fidelity global ionospheric model(s) for 3-satellite formation flying, which can potentially be used for new multi-scale ionospheric measurement mission design.